package simple;
import JaCoP.constraints.IfThen;
import JaCoP.constraints.XeqY;
import JaCoP.core.IntVar;
import JaCoP.core.Store;
import JaCoP.search.DepthFirstSearch;
import JaCoP.search.IndomainMin;
import JaCoP.search.Search;
import JaCoP.search.SelectChoicePoint;
import JaCoP.search.SimpleSelect;

public class FullAdder2 {

	/**
	 * @param args
	 */
	public static void main(String[] args) {
		long T1, T2, T;
		T1 = System.currentTimeMillis();
		fullAdd();
		T2 = System.currentTimeMillis();
		T = T2 - T1;
		System.out.println("\n\t*** Execution time = " + T + " ms");
	}

	private static void fullAdd() {
		Store store = new Store();
		/*
		 * Inverse carry module
		 */
		IntVar A = new IntVar(store, "In1", 0,1);
		IntVar B = new IntVar(store, "In2", 0,1);
		IntVar C = new IntVar(store, "CarryIn", 0,1);
		IntVar t1 = new IntVar(store, "T1", 0,1);
		IntVar t2 = new IntVar(store, "T2", 0,1);
		IntVar t3 = new IntVar(store, "T3", 0,1);
		IntVar t4 = new IntVar(store, "T4", 0,1);
		IntVar cOutInv = new IntVar(store, "CarryOutInverted", 0,1); 
		IntVar cOut = new IntVar(store, "CarryOut", 0,1);
		IntVar vdd = new IntVar(store, "VDD", 1,1);
		IntVar gnd = new IntVar(store, "Ground", 0,0);
		
		
		/*
		 * First column
		 */
		store.impose(new IfThen(new XeqY(A, gnd), new XeqY(vdd, t1)));
		store.impose(new IfThen(new XeqY(A, vdd), new XeqY(t2, gnd)));
		/*
		 * Second column
		 */
		store.impose(new IfThen(new XeqY(C, gnd), new XeqY(t1, cOutInv)));
		store.impose(new IfThen(new XeqY(C, vdd), new XeqY(cOutInv, t2)));
		/*
		 * Third column
		 */
		store.impose(new IfThen(new XeqY(B, gnd), new XeqY(vdd, t1)));
		store.impose(new IfThen(new XeqY(B, vdd), new XeqY(t2, gnd)));
		/*
		 * Fourth column
		 */
		store.impose(new IfThen(new XeqY(B, gnd), new XeqY(vdd, t3)));
		store.impose(new IfThen(new XeqY(A, gnd), new XeqY(t3, cOutInv)));
		store.impose(new IfThen(new XeqY(A, vdd), new XeqY(cOutInv, t4)));
		store.impose(new IfThen(new XeqY(B, vdd), new XeqY(t4, gnd)));
		
		/*
		 * Inverter module 1
		 */
		store.impose(new IfThen(new XeqY(cOutInv, gnd), new XeqY(vdd, cOut)));
		store.impose(new IfThen(new XeqY(cOutInv, vdd), new XeqY(gnd, cOut)));
		
		/*
		 * Inverse sum module
		 */
		IntVar sumInv = new IntVar(store, "SumInverted", 0,1);
		IntVar sum = new IntVar(store, "Sum",0,1);
		IntVar s1 = new IntVar(store, "S1", 0,1);
		IntVar s2 = new IntVar(store, "S2", 0,1);
		IntVar s3 = new IntVar(store, "S3", 0,1);
		IntVar s4 = new IntVar(store, "S4", 0,1);
		IntVar s5 = new IntVar(store, "S5", 0,1);
		IntVar s6 = new IntVar(store, "S6", 0,1);
		
		/*
		 * First column
		 */
		store.impose(new IfThen(new XeqY(A, gnd), new XeqY(vdd, s1)));
		store.impose(new IfThen(new XeqY(A, vdd), new XeqY(s2, gnd)));
		/*
		 * Second column
		 */
		store.impose(new IfThen(new XeqY(B, gnd), new XeqY(vdd, s1)));
		store.impose(new IfThen(new XeqY(cOutInv, gnd), new XeqY(s1, sumInv)));
		store.impose(new IfThen(new XeqY(cOutInv, vdd), new XeqY(sumInv, s2)));
		store.impose(new IfThen(new XeqY(B, vdd), new XeqY(s2, gnd)));
		/*
		 * Third column
		 */
		store.impose(new IfThen(new XeqY(C, gnd), new XeqY(vdd, s1)));
		store.impose(new IfThen(new XeqY(C, vdd), new XeqY(s2, gnd)));
		/*
		 * Fourth column
		 */
		store.impose(new IfThen(new XeqY(A, gnd), new XeqY(vdd, s3)));
		store.impose(new IfThen(new XeqY(B, gnd), new XeqY(s3, s4)));
		store.impose(new IfThen(new XeqY(C, gnd), new XeqY(s4, sumInv)));
		store.impose(new IfThen(new XeqY(C, vdd), new XeqY(sumInv, s5)));
		store.impose(new IfThen(new XeqY(B, vdd), new XeqY(s5, s6)));
		store.impose(new IfThen(new XeqY(A, vdd), new XeqY(s6, gnd)));
		
		/*
		 * Inverter module 2
		 */
		store.impose(new IfThen(new XeqY(sumInv, gnd), new XeqY(vdd, sum)));
		store.impose(new IfThen(new XeqY(sumInv, vdd), new XeqY(gnd, sum)));
		
		
		IntVar[] all = {A,B,C, cOut, sum};
		Search<IntVar> label = new DepthFirstSearch<IntVar>();
		SelectChoicePoint<IntVar> select = new SimpleSelect<IntVar>(all, null, new IndomainMin<IntVar>());
		label.getSolutionListener().searchAll(true); 
		label.getSolutionListener().recordSolutions(true);
		boolean Result = label.labeling(store, select);
		

		
		if(Result) {
			label.getSolutionListener().printAllSolutions();
		} else {
			System.out.println("\n*** No");
		}
		
		
	}

}
